$\forall$${\it es}$:ES, $A$, $B$:Type, $f$:($A$$\rightarrow$$B$), ${\it Ia}$:AbsInterface($A$). (E($f$'${\it Ia}$) $\subseteq$r E(${\it Ia}$)) \& (E(${\it Ia}$) $\subseteq$r E($f$'${\it Ia}$))